Inference at * 
Iof proof for Lemma decidable-filter:


  T:Type, L:(T List), P:({x:T| (x  L)} ).
  (xL. Dec(P(x)))  (L':T List. (L'  L & (x:T. (x  L')  ((x  L) & P(x))))) 

latex

 by ((InductionOnList) 
CollapseTHEN (Auto)) 

latex

C1: 

C1: 1. T : Type
C1: 2. T List
C1: 3. P : {x:T| (x  [])} 
C1: 4. x[]. Dec(P(x))
C1:   L':T List. (L'  [] & (x:T. (x  L')  ((x  []) & P(x))))
C2: 

C2: 1. T : Type
C2: 2. T List
C2: 3. u : T
C2: 4. v : T List
C2: 5. P:({x:T| (x  v)} ).
C2: 5. (xv. Dec(P(x)))  (L':T List. (L'  v & (x:T. (x  L')  ((x  v) & P(x)))))
C2: 6. P : {x:T| (x  [u / v])} 
C2: 7. x[u / v]. Dec(P(x))
C2:   L':T List. (L'  [u / v] & (x:T. (x  L')  ((x  [u / v]) & P(x))))
C.

Definitions	[], P  Q, P  Q, x:A. B(x), P  Q, P & Q, x:A  B(x), L1  L2, xL. P(x), x. t(x), x.A(x), Dec(P), x(s), f(a), {x:A| B(x)} , (x  l), [car / cdr], x:A. B(x), x:AB(x), s = t, A List, type List, t  T, , Type
Lemmas	iff wf, sublist wf, l all wf, decidable wf, l member wf